@conference{BCCZ99,
 author =       {A. Biere and A. Cimatti and E. Clarke and Y. Zhu.},
 title =        {Symbolic Model Checking without BDDs},
 booktitle = {Tools and Algorithms for Construction and Analysis
      of Systems, In TACAS'99},
 year = {March 1999}
}

@conference{CCG+02,
 author =       {A. Cimatti and E. Clarke and E. Giunchiglia and F.
 Giunchiglia and M. Pistore and M. Roveri and R. Sebastiani and A. Tacchella.},
 title =        {NuSMV 2: An OpenSource Tool for Symbolic Model
 Checking},
 booktitle = {Proceedings of Computer Aided Verification (CAV 02)},
 year = {2002}
}

@conference{CCGR00,
 author =       {A. Cimatti and E. Clarke and F. Giunchiglia and M. Roveri.},
 title =        {NuSMV: a new symbolic model checker.},
 booktitle = {International Journal on Software Tools for Technology
 Transfer (STTT), 2(4)},
 year = {March 2000}
}

@conference{BCLM+94,
 author =       {J.R. Burch and E.M. Clarke and D.E. Long and K.L. McMillan and D.L. Dill.},
 title =        {Symbolic Model Checking for Sequential Circuit Verification.},
 booktitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401--424},
 year = {April 1994}
}

@conference{CGH97,
 author =       {E. Clarke and O. Grumberg and K. Hamaguchi.},
 title =        {Another Look at LTL Model Checking},
 booktitle =  {Formal Methods in System Design, 10(1):57--71},
 year = { February 1997}
}

@conference{CMB90,
 author =       {O. Coudert and C. Berthet and J. C. Madre.},
 title =        {Verification of synchronous sequential machines based
 on symbolic execution},
 booktitle =  {In J. Sifakis, editor, Proceedings of the International
 Workshop on Automatic Verification Methods for Finite State Systems,
 volume 407 of LNCS, pages 365--373, Berlin},
 year = {June 1990}
}

@conference{Dil88,
 author =       {D. Dill.},
 title =        {Trace Theory for Automatic Hierarchical Verification
 of Speed-Independent Circuits},
 booktitle =  {ACM Distinguished Dissertations. MIT Press},
 year = {1988}
}

@conference{McMil92,
 author =       {K.L. McMillan.},
 title =        {The SMV system -- DRAFT},
 booktitle =  {Available at
 {\tt http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.r2.2.ps}},
 year = {1992 }
}

@conference{McMil93,
 author =       {K.L. McMillan.},
 title =        {Symbolic Model Checking},
 booktitle =  {Kluwer Academic Publ.},
 year = {1993 }
}

@conference{Mart85,
 author =       {A.J. Martin.},
 title =        {The design of a self-timed circuit for distributed
 mutual exclusion.},
 booktitle =  {In H. Fuchs and W.H. Freeman, editors,
 \emph{Proceedings of the 1985 Chapel Hill Conference on VLSI}, pages
 245--260, New York},
 year = {1985}
}

@conference{MOON00,
 author =       {Moon and Hachtel and Somenzi},
 title =        {Border-Block Tringular Form and Conjunction Schedule
 in Image Computation},
 booktitle =  {FMCAD},
 year = {2000}
}

@conference{RAP+95,
 author =       {R. K. Ranjan and A. Aziz and B. Plessier and C. Pixley and R.
 K. Brayton},
 title =        {Efficient BDD algorithms for FSM synthesis and
 verification},
 booktitle =  {In IEEE/ACM Proceedings International Workshop on
 Logic Synthesis,  Lake Tahoe (NV)},
 year = {May 1995 }
}

@conference{Som98,
 author =       {F. Somenzi},
 title =        {CUDD: CU Decision Diagram package --- release 2.2.0 },
 booktitle =  {Department of Electrical and Computer Engineering ---
 University of Colorado at Boulder},
 year = {May 1998}
}

@conference{Vis96,
 author =       {"VIS: A system for Verification and Synthesis", The VIS
 Group},
 title =        {Proceedings of the 8th International Conference on
 Computer Aided Verification, p428-432},
 booktitle =  {Springer Lecture Notes in Computer Science, 1102,
 Edited by R. Alur and T. Henzinger, New Brunswick, NJ},
 year = {1996}
}

@conference{EMSS91,
 author =       {E. Allen Emerson and A. K. Mok and A. Prasad Sistla and Jai
 Srinivasan},
 title =        {Quantitative temporal reasoning},
 booktitle =  {Edmund M. Clarke and Robert P. Krushan, editors,
 Proceedings of Computer-Aided Verification (CAV'90), volume 531 of
 LNCS, pages 136-145, Berlin, Germany},
 year = {June 1991}
}

@inproceedings{een04temporal,
    author = {Niklas E\'en and Niklas S\"orensson},
    title = {Temporal induction by incremental SAT solving},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    volume = {89},
    issue = {4},
    publisher = {Elsevier},
    editor = {Ofer Strichman and Armin Biere},
    year = {2004}
}

@Misc{PSLLRM,
  key = 	 {psllrm},
  title = 	 {{A}ccellera, {P}roperty {S}pecification {L}anguage - {R}eference {M}anual - {V}ersion 1.01},
  howpublished = {http://www.eda.org/vfv/docs/psl\_lrm-1.01.pdf},
  month = 	 {April},
  year = 	 {2003},
}

@Misc{PSLparser,
  key = 	 {PSLparser},
  title = 	 {{L}anguage {F}ront-{E}nd for {S}ugar {F}oundation {L}anguage},
  howpublished = {http://www.haifa.il.ibm.com/projects/verification/sugar/parser.html},
}


@inproceedings{vmcai05,
  author =       "T. Latvala and A. Biere and K. Heljanko and T. Junttila",
  title =        "Simple is Better: Efficient Bounded Model Checking for Past {LTL}",
  booktitle =    "{V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation, 6th International Conference {VMCAI} 2005",
  pages =        "380--395",
  year =         2005,
  editor =       "R. Cousot",
  number =       3385,
  series =       "Lecture Notes in Computer Science",
  publisher =    {Springer}
}

@inproceedings{cav05,
  author =       "K. Heljanko, T. Junttila and T. Latvala",
  title =        "Incremental and Complete Bounded Model Checking for Full {PLTL}",
  booktitle =    "Computer Aided Verification, 17$^{th}$ International Conference {CAV} 2005",
  pages =        "98--111",
  year =         2005,
  editor =       "K. Etessami and S.~K. Rajamani",
  number =       3576,
  series =       "Lecture Notes in Computer Science",
  publisher =    {Springer}
}

@inproceedings{fm06,

 author= {W. Johnston K. Winter L. van den Berg, P. A. Strooper and
          P. Robinson},
 title =  {Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking},
  booktitle =    "FM 2006: Formal Methods",
  pages =        "524--540",
  year =         2006,
  editor =       "",
  number =       4085,
  series =       "Lecture Notes in Computer Science",
  publisher =    {Springer Berlin}
}

@inproceedings{abdulla00symbolic,
  author    = {P.~A. Abdulla and P. Bjesse and N. E{\'e}n},
  title     = {Symbolic Reachability Analysis Based on SAT-Solvers.},
  booktitle = {Proceedings of Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000},
  pages     = {411-425},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1785},
  year      = {2000}
}


